<!DOCTYPE html>
<html class="writer-html5" lang="en" >
<head>
  <meta charset="utf-8" /><meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>header for testing &mdash; The Mechanics of Proof, by Heather Macbeth</title>
      <link rel="stylesheet" href="_static/pygments.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/custom.css" type="text/css" />
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
        <script src="_static/jquery.js"></script>
        <script src="_static/underscore.js"></script>
        <script src="_static/doctools.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >
            <a href="index.html" class="icon icon-home"> The Mechanics of Proof
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul>
<li class="toctree-l1"><a class="reference internal" href="00_Introduction.html">Preface</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="01_Proofs_by_Calculation.html">1. Proofs by calculation</a></li>
<li class="toctree-l1"><a class="reference internal" href="02_Proofs_with_Structure.html">2. Proofs with structure</a></li>
<li class="toctree-l1"><a class="reference internal" href="03_Parity_and_Divisibility.html">3. Parity and divisibility</a></li>
<li class="toctree-l1"><a class="reference internal" href="04_Proofs_with_Structure_II.html">4. Proofs with structure, II</a></li>
<li class="toctree-l1"><a class="reference internal" href="05_Logic.html">5. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="06_Induction.html">6. Induction</a></li>
<li class="toctree-l1"><a class="reference internal" href="07_Number_Theory.html">7. Number theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="08_Functions.html">8. Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="09_Sets.html">9. Sets</a></li>
<li class="toctree-l1"><a class="reference internal" href="10_Relations.html">10. Relations</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="Index_of_Tactics.html">Index of Lean tactics</a></li>
<li class="toctree-l1"><a class="reference internal" href="Mainstream_Lean.html">Transitioning to mainstream Lean</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">The Mechanics of Proof</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home"></a> &raquo;</li>
      <li>header for testing</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/latexindex.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="header-for-testing">
<h1>header for testing<a class="headerlink" href="#header-for-testing" title="Permalink to this headline">&#61633;</a></h1>
<div class="toctree-wrapper compound">
<ul>
<li class="toctree-l1"><a class="reference internal" href="00_Introduction.html">Preface</a><ul>
<li class="toctree-l2"><a class="reference internal" href="00_Introduction.html#about-this-book">About this book</a></li>
<li class="toctree-l2"><a class="reference internal" href="00_Introduction.html#why-lean">Why Lean?</a></li>
<li class="toctree-l2"><a class="reference internal" href="00_Introduction.html#contents-and-prerequisites">Contents and prerequisites</a></li>
<li class="toctree-l2"><a class="reference internal" href="00_Introduction.html#note-for-instructors">Note for instructors</a></li>
<li class="toctree-l2"><a class="reference internal" href="00_Introduction.html#acknowledgements">Acknowledgements</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="01_Proofs_by_Calculation.html">1. Proofs by calculation</a><ul>
<li class="toctree-l2"><a class="reference internal" href="01_Proofs_by_Calculation.html#proving-equalities">1.1. Proving equalities</a></li>
<li class="toctree-l2"><a class="reference internal" href="01_Proofs_by_Calculation.html#proving-equalities-in-lean">1.2. Proving equalities in Lean</a></li>
<li class="toctree-l2"><a class="reference internal" href="01_Proofs_by_Calculation.html#tips-and-tricks">1.3. Tips and tricks</a></li>
<li class="toctree-l2"><a class="reference internal" href="01_Proofs_by_Calculation.html#proving-inequalities">1.4. Proving inequalities</a></li>
<li class="toctree-l2"><a class="reference internal" href="01_Proofs_by_Calculation.html#a-shortcut">1.5. A shortcut</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="02_Proofs_with_Structure.html">2. Proofs with structure</a><ul>
<li class="toctree-l2"><a class="reference internal" href="02_Proofs_with_Structure.html#intermediate-steps">2.1. Intermediate steps</a></li>
<li class="toctree-l2"><a class="reference internal" href="02_Proofs_with_Structure.html#invoking-lemmas">2.2. Invoking lemmas</a></li>
<li class="toctree-l2"><a class="reference internal" href="02_Proofs_with_Structure.html#or-and-proof-by-cases">2.3. &#8220;Or&#8221; and proof by cases</a></li>
<li class="toctree-l2"><a class="reference internal" href="02_Proofs_with_Structure.html#and">2.4. &#8220;And&#8221;</a></li>
<li class="toctree-l2"><a class="reference internal" href="02_Proofs_with_Structure.html#existence-proofs">2.5. Existence proofs</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="03_Parity_and_Divisibility.html">3. Parity and divisibility</a><ul>
<li class="toctree-l2"><a class="reference internal" href="03_Parity_and_Divisibility.html#definitions-parity">3.1. Definitions; parity</a></li>
<li class="toctree-l2"><a class="reference internal" href="03_Parity_and_Divisibility.html#divisibility">3.2. Divisibility</a></li>
<li class="toctree-l2"><a class="reference internal" href="03_Parity_and_Divisibility.html#modular-arithmetic-theory">3.3. Modular arithmetic: theory</a></li>
<li class="toctree-l2"><a class="reference internal" href="03_Parity_and_Divisibility.html#modular-arithmetic-calculations">3.4. Modular arithmetic: calculations</a></li>
<li class="toctree-l2"><a class="reference internal" href="03_Parity_and_Divisibility.html#bezout-s-identity">3.5. B&#233;zout&#8217;s identity</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="04_Proofs_with_Structure_II.html">4. Proofs with structure, II</a><ul>
<li class="toctree-l2"><a class="reference internal" href="04_Proofs_with_Structure_II.html#for-all-and-implication">4.1. &#8220;For all&#8221; and implication</a></li>
<li class="toctree-l2"><a class="reference internal" href="04_Proofs_with_Structure_II.html#if-and-only-if">4.2. &#8220;If and only if&#8221;</a></li>
<li class="toctree-l2"><a class="reference internal" href="04_Proofs_with_Structure_II.html#there-exists-a-unique">4.3. &#8220;There exists a unique&#8221;</a></li>
<li class="toctree-l2"><a class="reference internal" href="04_Proofs_with_Structure_II.html#contradictory-hypotheses">4.4. Contradictory hypotheses</a></li>
<li class="toctree-l2"><a class="reference internal" href="04_Proofs_with_Structure_II.html#proof-by-contradiction">4.5. Proof by contradiction</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="05_Logic.html">5. Logic</a><ul>
<li class="toctree-l2"><a class="reference internal" href="05_Logic.html#logical-equivalence">5.1. Logical equivalence</a></li>
<li class="toctree-l2"><a class="reference internal" href="05_Logic.html#the-law-of-the-excluded-middle">5.2. The law of the excluded middle</a></li>
<li class="toctree-l2"><a class="reference internal" href="05_Logic.html#normal-form-for-negations">5.3. Normal form for negations</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="06_Induction.html">6. Induction</a><ul>
<li class="toctree-l2"><a class="reference internal" href="06_Induction.html#introduction">6.1. Introduction</a></li>
<li class="toctree-l2"><a class="reference internal" href="06_Induction.html#recurrence-relations">6.2. Recurrence relations</a></li>
<li class="toctree-l2"><a class="reference internal" href="06_Induction.html#two-step-induction">6.3. Two-step induction</a></li>
<li class="toctree-l2"><a class="reference internal" href="06_Induction.html#strong-induction">6.4. Strong induction</a></li>
<li class="toctree-l2"><a class="reference internal" href="06_Induction.html#pascal-s-triangle">6.5. Pascal&#8217;s triangle</a></li>
<li class="toctree-l2"><a class="reference internal" href="06_Induction.html#the-division-algorithm">6.6. The Division Algorithm</a></li>
<li class="toctree-l2"><a class="reference internal" href="06_Induction.html#the-euclidean-algorithm">6.7. The Euclidean algorithm</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="07_Number_Theory.html">7. Number theory</a><ul>
<li class="toctree-l2"><a class="reference internal" href="07_Number_Theory.html#infinitely-many-primes">7.1. Infinitely many primes</a></li>
<li class="toctree-l2"><a class="reference internal" href="07_Number_Theory.html#gauss-and-euclid-s-lemmas">7.2. Gauss&#8217; and Euclid&#8217;s lemmas</a></li>
<li class="toctree-l2"><a class="reference internal" href="07_Number_Theory.html#the-square-root-of-two">7.3. The square root of two</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="08_Functions.html">8. Functions</a><ul>
<li class="toctree-l2"><a class="reference internal" href="08_Functions.html#injectivity-and-surjectivity">8.1. Injectivity and surjectivity</a></li>
<li class="toctree-l2"><a class="reference internal" href="08_Functions.html#bijectivity">8.2. Bijectivity</a></li>
<li class="toctree-l2"><a class="reference internal" href="08_Functions.html#composition-of-functions">8.3. Composition of functions</a></li>
<li class="toctree-l2"><a class="reference internal" href="08_Functions.html#product-types">8.4. Product types</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="09_Sets.html">9. Sets</a><ul>
<li class="toctree-l2"><a class="reference internal" href="09_Sets.html#introduction">9.1. Introduction</a></li>
<li class="toctree-l2"><a class="reference internal" href="09_Sets.html#set-operations">9.2. Set operations</a></li>
<li class="toctree-l2"><a class="reference internal" href="09_Sets.html#the-type-of-sets">9.3. The type of sets</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="10_Relations.html">10. Relations</a><ul>
<li class="toctree-l2"><a class="reference internal" href="10_Relations.html#reflexive-symmetric-antisymmetric-transitive">10.1. Reflexive, symmetric, antisymmetric, transitive</a></li>
<li class="toctree-l2"><a class="reference internal" href="10_Relations.html#equivalence-relations">10.2. Equivalence relations</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="Index_of_Tactics.html">Index of Lean tactics</a></li>
<li class="toctree-l1"><a class="reference internal" href="Mainstream_Lean.html">Transitioning to mainstream Lean</a></li>
</ul>
</div>
</section>


           </div>
          </div>
          <footer>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2022-2024, Heather Macbeth.  All rights reserved.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>